Inference at * 2 
Iof proof for Lemma member nth tl:

.....upcase..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
  x:T, L:(T List). (x  nth_tl(n;L))  (x  L) 

latex

 by InductionOnList 

latex

 1: 

 1: 5. x : T
 1: 6. T List
 1:   (x  nth_tl(n;[]))  (x  [])
 2: 

 2: 5. x : T
 2: 6. T List
 2: 7. u : T
 2: 8. v : T List
 2: 9. (x  nth_tl(n;v))  (x  v)
 2:   (x  nth_tl(n;[u / v]))  (x  [u / v])
 .

Definitions	P  Q, (x  l), x:A. B(x), x:AB(x), a < b, , Type, s = t, t  T, type List
Lemmas	l member wf